Computer-aided design (CAD) of digital circuits using large scale programmed digital computers is a well-developed technology. Several techniques are used in digital circuitry CAD for extracting more information about the logic signal value assignments and logical interrelations among the logic gates in a proposed or existing digital circuit. Logic design analysis is used in CAD to determine logical interconnections and interdependencies between logic gates based on the structural topology of a digital circuit. An important part of this process is identifying all signal values that can be implied both directly and indirectly as a result of a given situation of value assignments. This includes recognition of various simple and complex physical and logical relations among two or more logic gates in the circuit as a result of a given situation of value assignments.
This analysis process is commonly referred to as learning and the logical interconnections and interdependencies are called implications. As examples, automatic test pattern generation (ATPG) for digital circuits, logic hardware optimization, logic hardware timing analysis and digital circuit engineering changes (EC) require logic design analysis. A problem encountered in CAD is the computational resources required both in terms of time and memory space. This is because all of the above-mentioned CAD problems may require the computer system to explore every possible input value to the circuit which may be exponential in number, commonly referred to as NP-complete or intractable. Hence, in the worst case, they require an exponential amount of time and/or memory space for a complete solution to be found. Therefore, good, efficient heuristics or shortcuts must be designed to solve these problems.
Consider digital circuit design verification. It is commonly performed using binary decision diagram (BDD) data representations, as shown in S. Malik et al., Logic Verification Using Binary Decision Diagrams in a Logic Synthesis Environment, Int'l Conf. on Computer-Aided Design, pp. 6-9 (1988); and M. Fujita et al., Evaluation and Improvements of Boolean Comparison Methods Based on Binary Decision Diagrams, Int'l Conf. on Computer-Aided Design, pp. 2-5 (1988). Such BDD-based verification processes are most advantageous to use when the logic designs being compared have few to none known logical interconnections. When the logic designs have numerous similarities, the designs are often verified using techniques that find constant valued relationships among the logic gates, such as shown in C. L. Berman & L. H. Trevyllian, Functional Comparison of Logic Designs for VLSI Circuits, Int'l Conf. on Computer-Aided Design, pp. 456-59 (1989); D. Brand, Verification of Large Synthesized Designs, Int'l Conf. on Computer-Aided Design, pp. 534-37 (1993); E. Cerny & C. Mauras, Tautology Checking Using Cross-Controllability and Cross-Observability Relations, ICCAD, pp. 34-38 (1990); and W. Kunz, HANNIBAL: An Efficient Tool for Logic Verification Based on Recursive Learning, Int'l Conf. on Computer-Aided Design (1993).
Implication-based verification systems basically operate in two phases. During Phase I, implications that occur between the logic gates comprising the two circuits being verified are learned. These implications include the discovery of logically equivalent and logically inverse signals or gate outputs between the two circuits. The circuit is analyzed using a different number of learning levels.
During Phase II, the learned implications are used to prove equivalency by examining a portion of the circuit situated between some set of internal logic gates and the primary outputs.
The difficulty with some of these approaches is that the computational time required increases exponentially with the number of learning levels analyzed. Current techniques show that the application of these techniques to five or more levels is impracticable because the technique is severely exponentially expensive with the number of learning levels being analyzed.
Thus, finding logical interconnections in which a constant Boolean value asserted at one logic gate causes (or implies) another constant Boolean signal (or value) at another logically or physically interconnected logic gate can be computationally inefficient for large circuit designs. These techniques are not general enough to detect other types of useful implications which are not constant valued.
Further, these techniques will fail to verify a design if only a portion of the circuit is examined during Phase II, where there is an insufficient number of implications, the nature of the implications is unsatisfactory, or the portion of the circuit being examined is incomplete. An "incomplete" partition immediately precludes the verification of the two circuits by analysis of the portion of the circuit lying between the cutset and the primary outputs of the two circuits. Note, in the worst case, the functional learning techniques can also require exponential time to identify some logical relations. This is because the underlying problem is NP-complete.
Another important problem in the CAD industry is that of ATPG for deriving test vectors for fabrication faults in digital circuits. A special type of fault is called a redundant fault. These faults are often too hard for ordinary ATPG tools to detect. In some cases, more efficient analysis of the logic interrelations among the logic gates in the circuit is required by means of learning techniques. Hence, learning-based ATPG tools perform much better on redundant and hard-to-detect faults, such as shown in Schulz et al., SOCRATES: A Highly Efficient Automatic Test Pattern Generation System, Int'l Test Conf. (1987). The relations and constraints that are discovered by learning techniques prune the search space for a test vector for the targeted fault. However, these tools are restricted by the use of only constant valued learning, some of which in current techniques may take unnecessarily excessive computational resources in being discovered.
Accordingly, there is a need for a computer-aided design system and method thereof to perform logic design analysis for determining logical interdependencies between points in a digital circuit topology, to verify whether digital circuits are equivalent, to decrease computational resources for the construction of a representation of a hardware design, and to perform goal directed learning in a digital circuit, that is more immune to the number of gate levels to thereby increase the speed of processing, decrease the amount of time required, and decrease the amount of memory space needed for processing.
Accordingly, there is a need for a computer-aided design system and method thereof to enable the solving of problems when a digital circuit is a large and complex topology of logic gates.
Accordingly, there is a need for a computer-aided design system and method thereof that can find both constant valued and functional valued implications.
Also, there is a need for a computer-aided design system and method thereof that can determine whether a partition of one of a pair of digital circuits being verified is inadequate (incomplete) or complete.